/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
-/
import Mathlib.Data.Set.Piecewise
import Mathlib.Order.Filter.Basic

/-!
# Definition of `Filter.atTop` and `Filter.atBot` filters

In this file we define the filters

* `Filter.atTop`: corresponds to `n → +∞`;
* `Filter.atBot`: corresponds to `n → -∞`.
-/

assert_not_exists Finset

variable {ι ι' α β γ : Type*}

open Set

namespace Filter

/-- `atTop` is the filter representing the limit `→ ∞` on an ordered set.
  It is generated by the collection of up-sets `{b | a ≤ b}`.
  (The preorder need not have a top element for this to be well defined,
  and indeed is trivial when a top element exists.) -/
def atTop [Preorder α] : Filter α :=
  ⨅ a, 𝓟 (Ici a)

/-- `atBot` is the filter representing the limit `→ -∞` on an ordered set.
  It is generated by the collection of down-sets `{b | b ≤ a}`.
  (The preorder need not have a bottom element for this to be well defined,
  and indeed is trivial when a bottom element exists.) -/
def atBot [Preorder α] : Filter α :=
  ⨅ a, 𝓟 (Iic a)

theorem mem_atTop [Preorder α] (a : α) : { b : α | a ≤ b } ∈ @atTop α _ :=
  mem_iInf_of_mem a <| Subset.refl _

theorem Ici_mem_atTop [Preorder α] (a : α) : Ici a ∈ (atTop : Filter α) :=
  mem_atTop a

theorem Ioi_mem_atTop [Preorder α] [NoTopOrder α] (x : α) : Ioi x ∈ (atTop : Filter α) :=
  let ⟨z, hz⟩ := exists_not_le x
  mem_of_superset (inter_mem (mem_atTop x) (mem_atTop z))
    fun _ ⟨hxy, hzy⟩ => lt_of_le_not_ge hxy fun hyx => hz (hzy.trans hyx)

theorem mem_atBot [Preorder α] (a : α) : { b : α | b ≤ a } ∈ @atBot α _ :=
  mem_iInf_of_mem a <| Subset.refl _

theorem Iic_mem_atBot [Preorder α] (a : α) : Iic a ∈ (atBot : Filter α) :=
  mem_atBot a

theorem Iio_mem_atBot [Preorder α] [NoBotOrder α] (x : α) : Iio x ∈ (atBot : Filter α) :=
  let ⟨z, hz⟩ := exists_not_ge x
  mem_of_superset (inter_mem (mem_atBot x) (mem_atBot z))
    fun _ ⟨hyx, hyz⟩ => lt_of_le_not_ge hyx fun hxy => hz (hxy.trans hyz)

theorem eventually_ge_atTop [Preorder α] (a : α) : ∀ᶠ x in atTop, a ≤ x :=
  mem_atTop a

theorem eventually_le_atBot [Preorder α] (a : α) : ∀ᶠ x in atBot, x ≤ a :=
  mem_atBot a

theorem eventually_gt_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, a < x :=
  Ioi_mem_atTop a

theorem eventually_ne_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, x ≠ a :=
  (eventually_gt_atTop a).mono fun _ => ne_of_gt

theorem eventually_lt_atBot [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x < a :=
  Iio_mem_atBot a

theorem eventually_ne_atBot [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x ≠ a :=
  (eventually_lt_atBot a).mono fun _ => ne_of_lt

theorem _root_.IsTop.atTop_eq [Preorder α] {a : α} (ha : IsTop a) : atTop = 𝓟 (Ici a) :=
  (iInf_le _ _).antisymm <| le_iInf fun b ↦ principal_mono.2 <| Ici_subset_Ici.2 <| ha b

theorem _root_.IsBot.atBot_eq [Preorder α] {a : α} (ha : IsBot a) : atBot = 𝓟 (Iic a) :=
  ha.toDual.atTop_eq

theorem atTop_eq_generate_Ici [Preorder α] : atTop = generate (range (Ici (α := α))) := by
  simp only [generate_eq_biInf, atTop, iInf_range]

theorem Frequently.forall_exists_of_atTop [Preorder α] {p : α → Prop}
    (h : ∃ᶠ x in atTop, p x) (a : α) : ∃ b ≥ a, p b := by
  rw [Filter.Frequently] at h
  contrapose! h
  exact (eventually_ge_atTop a).mono h

theorem Frequently.forall_exists_of_atBot [Preorder α] {p : α → Prop}
    (h : ∃ᶠ x in atBot, p x) (a : α) : ∃ b ≤ a, p b :=
  Frequently.forall_exists_of_atTop (α := αᵒᵈ) h _

lemma atTop_eq_generate_of_forall_exists_le [Preorder α] {s : Set α} (hs : ∀ x, ∃ y ∈ s, x ≤ y) :
    (atTop : Filter α) = generate (Ici '' s) := by
  rw [atTop_eq_generate_Ici]
  apply le_antisymm
  · rw [le_generate_iff]
    rintro - ⟨y, -, rfl⟩
    exact mem_generate_of_mem ⟨y, rfl⟩
  · rw [le_generate_iff]
    rintro - ⟨x, -, -, rfl⟩
    rcases hs x with ⟨y, ys, hy⟩
    have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
    have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
    exact sets_of_superset (generate (Ici '' s)) A B

lemma atTop_eq_generate_of_not_bddAbove [LinearOrder α] {s : Set α} (hs : ¬ BddAbove s) :
    (atTop : Filter α) = generate (Ici '' s) := by
  refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_
  obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x
  exact ⟨y, hy, hy'.le⟩

end Filter

open Filter

theorem Monotone.piecewise_eventually_eq_iUnion {β : α → Type*} [Preorder ι] {s : ι → Set α}
    [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋃ i, s i)]
    (hs : Monotone s) (f g : (a : α) → β a) (a : α) :
    ∀ᶠ i in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a := by
  rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
  · refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
    simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]
  · filter_upwards with i
    simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true, exists_false]

theorem Antitone.piecewise_eventually_eq_iInter {β : α → Type*} [Preorder ι] {s : ι → Set α}
    [∀ i, DecidablePred (· ∈ s i)] [DecidablePred (· ∈ ⋂ i, s i)]
    (hs : Antitone s) (f g : (a : α) → β a) (a : α) :
    ∀ᶠ i in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a := by
  classical
  convert ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]
